SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Z notation</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Z notation</span></span>

</h1>

</header>

</p>

<p>The <b>Z notation</b> <span class="rt-commentedText nowrap"><span class="IPA nopopups noexcerpt" lang="en-fonipa">/<span style="border-bottom:1px dotted"><span title="/ˈ/: primary stress follows">ˈ</span><span title="'z' in 'zoom'">z</span><span title="/ɛ/: 'e' in 'dress'">ɛ</span><span title="'d' in 'dye'">d</span></span>/</span></span> is a <a href="Formal_specification" title="Formal specification">formal</a> <a href="Specification_language" title="Specification language">specification language</a> used for describing and modelling computing systems.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> It is targeted at the clear specification of <a href="Computer_program" title="Computer program">computer programs</a> and computer-based systems in general.

</p>

<div class="mw-heading mw-heading2"><h2 id="History">History</h2></div>

<p>In 1974, <a href="Jean-Raymond_Abrial" title="Jean-Raymond Abrial">Jean-Raymond Abrial</a> published "Data Semantics".<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> He used a notation that would later be taught in the <a href="University_of_Grenoble" class="mw-redirect" title="University of Grenoble">University of Grenoble</a> until the end of the 1980s. While at EDF (<a href="%C3%89lectricit%C3%A9_de_France" title="Électricité de France">Électricité de France</a>), working with <a href="Bertrand_Meyer" title="Bertrand Meyer">Bertrand Meyer</a>, Abrial also worked on developing Z.<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> The Z notation is used in the 1980 book <i>Méthodes de programmation</i>.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup>

</p><p>Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and <a href="Bertrand_Meyer" title="Bertrand Meyer">Bertrand Meyer</a>.<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> It was developed further at the <a href="Programming_Research_Group" title="Programming Research Group">Programming Research Group</a> at <a href="Oxford_University" class="mw-redirect" title="Oxford University">Oxford University</a>, where Abrial worked in the early 1980s, having arrived at Oxford in September 1979.

</p><p>Abrial has said that Z is so named "Because it is the ultimate language!"<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup> although the name "<a href="Ernst_Zermelo" title="Ernst Zermelo">Zermelo</a>" is also associated with the Z notation through its use of <a href="Zermelo%E2%80%93Fraenkel_set_theory" title="Zermelo–Fraenkel set theory">Zermelo–Fraenkel set theory</a>.

</p><p>In 1992, the <a href="Z_User_Group" title="Z User Group">Z User Group</a> (ZUG) was established to oversee activities concerning the Z notation, especially meetings and conferences.<sup id="cite_ref-zug22_7-0" class="reference"><a href="#cite_note-zug22-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Usage_and_notation">Usage and notation</h2></div>

<p>Z is based on the standard mathematical notation used in <a href="Axiomatic_set_theory" class="mw-redirect" title="Axiomatic set theory">axiomatic set theory</a>, <a href="Lambda_calculus" title="Lambda calculus">lambda calculus</a>, and <a href="First-order_predicate_logic" class="mw-redirect" title="First-order predicate logic">first-order predicate logic</a>.<sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup> All expressions in Z notation are <a href="Type_(model_theory)" title="Type (model theory)">typed</a>, thereby avoiding some of the <a href="Naive_set_theory#Paradoxes" title="Naive set theory">paradoxes of naive set theory</a>. Z contains a standardized catalogue (called the <i>mathematical toolkit</i>) of commonly used mathematical functions and predicates, defined using Z itself. It is augmented with <b>Z schema</b> boxes, which can be combined using their own operators, based on standard logical operators, and also by including schemas within other schemas. This allows Z specifications to be built up into large specifications in a convenient manner.

</p><p>Because Z notation uses many non-<a href="ASCII" title="ASCII">ASCII</a> symbols, the specification includes suggestions for rendering the Z notation symbols in <a href="ASCII" title="ASCII">ASCII</a> and in <a href="LaTeX" title="LaTeX">LaTeX</a>. There are also <a href="Unicode" title="Unicode">Unicode</a> encodings for all standard Z symbols.<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Standards">Standards</h2></div>

<p><a href="International_Organization_for_Standardization" title="International Organization for Standardization">ISO</a> completed a Z standardization effort in 2002. This standard<sup id="cite_ref-Standard_10-0" class="reference"><a href="#cite_note-Standard-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup> and a technical corrigendum<sup id="cite_ref-Corrigendum_11-0" class="reference"><a href="#cite_note-Corrigendum-11"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup> are available from ISO free:

</p>

<ul><li>the standard is publicly available<sup id="cite_ref-Standard_10-1" class="reference"><a href="#cite_note-Standard-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup> from the ISO ITTF site free of charge and, separately, available for purchase<sup id="cite_ref-Standard_10-2" class="reference"><a href="#cite_note-Standard-10"><span class="cite-bracket">[</span>10<span class="cite-bracket">]</span></a></sup> from the ISO site;</li>

<li>the technical corrigendum is available<sup id="cite_ref-Corrigendum_11-1" class="reference"><a href="#cite_note-Corrigendum-11"><span class="cite-bracket">[</span>11<span class="cite-bracket">]</span></a></sup> from the ISO site free of charge.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Award">Award</h2></div>

<p>In 1992, <a href="Oxford_University_Computing_Laboratory" class="mw-redirect" title="Oxford University Computing Laboratory">Oxford University Computing Laboratory</a> and <a href="IBM" title="IBM">IBM</a> were jointly awarded The Queen's Award for Technological Achievement "for the development of ... the Z notation, and its application in the IBM Customer Information Control System (<a href="CICS" title="CICS">CICS</a>) product."<sup id="cite_ref-12" class="reference"><a href="#cite_note-12"><span class="cite-bracket">[</span>12<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFSpivey1992" class="citation book cs1"><a href="John_Michael_Spivey" class="mw-redirect" title="John Michael Spivey">Spivey, John Michael</a> (1992). <a rel="nofollow" class="external text" href="https://spivey.oriel.ox.ac.uk/corner/Z_Reference_Manual"><i>The Z Notation: A reference manual</i></a>. International Series in Computer Science (2nd ed.). <a href="Prentice_Hall" title="Prentice Hall">Prentice Hall</a>.</cite></li>

<li><cite id="CITEREFDaviesWoodcock1996" class="citation book cs1"><a href="Jim_Davies_(computer_scientist)" title="Jim Davies (computer scientist)">Davies, Jim</a>; <a href="Jim_Woodcock" title="Jim Woodcock">Woodcock, Jim</a> (1996). <a rel="nofollow" class="external text" href="https://web.archive.org/web/20070405133311/http://www.usingz.com/"><i>Using Z: Specification, Refinement and Proof</i></a>. International Series in Computer Science. Prentice Hall. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-13-948472-8</bdi>. Archived from <a rel="nofollow" class="external text" href="http://www.usingz.com/">the original</a> on 5 April 2007<span class="reference-accessdate">. Retrieved <span class="nowrap">22 March</span> 2006</span>.</cite></li>

<li><cite id="CITEREFBowen1996" class="citation book cs1"><a href="Jonathan_Bowen" title="Jonathan Bowen">Bowen, Jonathan</a> (1996). <a rel="nofollow" class="external text" href="https://www.researchgate.net/publication/2480325"><i>Formal Specification and Documentation using Z: A Case Study Approach</i></a>. International Thomson Computer Press, <a href="International_Thomson_Publishing" class="mw-redirect" title="International Thomson Publishing">International Thomson Publishing</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>1-85032-230-9</bdi>.</cite></li>

<li><cite id="CITEREFJacky1997" class="citation book cs1">Jacky, Jonathan (1997). <a rel="nofollow" class="external text" href="https://staff.washington.edu/jon/z-book/"><i>The Way of Z: Practical Programming with Formal Methods</i></a>. <a href="Cambridge_University_Press" title="Cambridge University Press">Cambridge University Press</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-521-55976-6</bdi>.</cite></li>

<li><cite id="CITEREFInce1993" class="citation book cs1">Ince, D. C. (1993). <i>An Introduction to Discrete Mathematics, Formal System Specification, and Z</i>. <a href="Oxford_University_Press" title="Oxford University Press">Oxford University Press</a>. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1093%2Foso%2F9780198538370.001.0001">10.1093/oso/9780198538370.001.0001</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0198538370</bdi>.</cite></li></ul>

<ul><li><a href="Z_User_Group" title="Z User Group">Z User Group</a> (ZUG)</li>

<li><a href="Community_Z_Tools" title="Community Z Tools">Community Z Tools</a> (CZT) project</li>

<li>Other <a href="Formal_methods" title="Formal methods">formal methods</a> (and languages using <a href="Formal_specification" title="Formal specification">formal specifications</a>):

<ul><li><a href="VDM-SL" class="mw-redirect" title="VDM-SL">VDM-SL</a>, the main alternative to Z</li>

<li><a href="B-Method" title="B-Method">B-Method</a>, developed by Jean-Raymond Abrial (creator of Z notation)</li>

<li><a href="Z%2B%2B" title="Z++">Z++</a> and <a href="Object-Z" title="Object-Z">Object-Z</a>, object extensions for the Z notation</li>

<li><a href="Alloy_(specification_language)" title="Alloy (specification language)">Alloy</a>, a specification language inspired by Z notation and implementing the principles of <a href="Object_Constraint_Language" title="Object Constraint Language">Object Constraint Language</a> (OCL)</li></ul></li>

<li><a href="Fastest" title="Fastest">Fastest</a>, a <a href="Model-based_testing" title="Model-based testing">model-based testing</a> tool for the Z notation</li>

<li><a href="Unified_Modeling_Language" title="Unified Modeling Language">Unified Modeling Language</a>, a software system design modeling tool by <a href="Object_Management_Group" title="Object Management Group">Object Management Group</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text"><cite id="CITEREFBowen2016" class="citation book cs1"><a href="Jonathan_Bowen" title="Jonathan Bowen">Bowen, Jonathan P.</a> (2016). <a rel="nofollow" class="external text" href="http://researchopen.lsbu.ac.uk/395/1/setss2014.pdf">"The Z Notation: Whence the Cause and Whither the Course?"</a> <span class="cs1-format">(PDF)</span>. <i>Engineering Trustworthy Software Systems</i>. <a href="Lecture_Notes_in_Computer_Science" title="Lecture Notes in Computer Science">Lecture Notes in Computer Science</a>. Vol. 9506. <a href="Springer_Science%2BBusiness_Media" title="Springer Science+Business Media">Springer</a>. pp. <span class="nowrap">103–</span>151. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-319-29628-9_3">10.1007/978-3-319-29628-9_3</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-319-29627-2</bdi>.</cite></span>

</li>

<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><cite id="CITEREFAbrial1974" class="citation cs2"><a href="Jean-Raymond_Abrial" title="Jean-Raymond Abrial">Abrial, Jean-Raymond</a> (1974), "Data Semantics", in Klimbie, J. W.; Koffeman, K. L. (eds.), <i>Proceedings of the <a href="IFIP" class="mw-redirect" title="IFIP">IFIP</a> Working Conference on Data Base Management</i>, <a href="North-Holland_Publishing_Company" class="mw-redirect" title="North-Holland Publishing Company">North-Holland</a>, pp. <span class="nowrap">1–</span>59</cite></span>

</li>

<li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><cite id="CITEREFHoare2011" class="citation book cs1"><a href="Tony_Hoare" title="Tony Hoare">Hoare, Tony</a> (2011). <a rel="nofollow" class="external text" href="https://link.springer.com/content/pdf/bbm%3A978-3-642-15187-3%2F1.pdf">"Greetings to Bertrand on the Occasion of his Sixtieth Birthday"</a> <span class="cs1-format">(PDF)</span>. In Nanz, Sebastian (ed.). <i>The Future of Software Engineering</i>. <a href="Springer_Science%2BBusiness_Media" title="Springer Science+Business Media">Springer</a>. pp. <span class="nowrap">183–</span>184. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-642-15187-3">10.1007/978-3-642-15187-3</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-3-642-15187-3</bdi>.</cite></span>

</li>

<li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><cite id="CITEREFMeyerBaudoin1980" class="citation cs2 cs1-prop-foreign-lang-source"><a href="Bertrand_Meyer" title="Bertrand Meyer">Meyer, Bertrand</a>; Baudoin, Claude (1980), <i>Méthodes de programmation</i> (in French), Eyrolles</cite></span>

</li>

<li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text"><cite id="CITEREFAbrialSchumanMeyer1980" class="citation cs2">Abrial, Jean-Raymond; Schuman, Stephen A; Meyer, Bertrand (1980), "A Specification Language", in Macnaghten, A. M.; McKeag, R. M. (eds.), <i>On the Construction of Programs</i>, <a href="Cambridge_University_Press" title="Cambridge University Press">Cambridge University Press</a>, <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>0-521-23090-X</bdi></cite> (describes early version of the language).</span>

</li>

<li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><cite id="CITEREFHoogeboom" class="citation web cs1">Hoogeboom, Hendrik Jan. <a rel="nofollow" class="external text" href="http://liacs.leidenuniv.nl/~hoogeboomhj/praatjes/formalmethods/formalmethods.pdf">"Formal Methods in Software Engineering"</a> <span class="cs1-format">(PDF)</span>. The Netherland: <a href="University_of_Leiden" class="mw-redirect" title="University of Leiden">University of Leiden</a><span class="reference-accessdate">. Retrieved <span class="nowrap">14 April</span> 2017</span>.</cite></span>

</li>

<li id="cite_note-zug22-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-zug22_7-0">^</a></b></span> <span class="reference-text"><cite id="CITEREFBowen2022" class="citation news cs1"><a href="Jonathan_Bowen" title="Jonathan Bowen">Bowen, Jonathan</a> (July 2022). <a rel="nofollow" class="external text" href="https://www.bcs.org/media/9401/facs-jul22.pdf">"The Z User Group: Thirty Years After"</a> <span class="cs1-format">(PDF)</span>. <i><a href="FACS_FACTS" class="mw-redirect" title="FACS FACTS">FACS FACTS</a></i>. No. <span class="nowrap">2022–</span>2. <a href="BCS-FACS" title="BCS-FACS">BCS-FACS</a>. pp. <span class="nowrap">50–</span>56<span class="reference-accessdate">. Retrieved <span class="nowrap">3 August</span> 2022</span>.</cite></span>

</li>

<li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text"><cite id="CITEREFSpivey1992" class="citation book cs1"><a href="Michael_Spivey" title="Michael Spivey">Spivey, J. Michael</a> (1992). <i>The Z Notation: A Reference Manual</i>. International Series in Computer Science (2nd ed.). Hemel Hempstead: <a href="Prentice_Hall" title="Prentice Hall">Prentice Hall</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-0139785290</bdi>.</cite></span>

</li>

<li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text"><cite id="CITEREFKorpela" class="citation web cs1">Korpela, Jukka K. <a rel="nofollow" class="external text" href="https://unicode-search.net/unicode-namesearch.pl?term=Z%20NOTATION">"Unicode Explained: Internationalize Documents, Programs, and Web Sites"</a>. <i>unicode-search.net</i><span class="reference-accessdate">. Retrieved <span class="nowrap">24 March</span> 2020</span>.</cite></span>

</li>

<li id="cite_note-Standard-10"><span class="mw-cite-backlink">^ <a href="#cite_ref-Standard_10-0"><sup><i><b>a</b></i></sup></a> <a href="#cite_ref-Standard_10-1"><sup><i><b>b</b></i></sup></a> <a href="#cite_ref-Standard_10-2"><sup><i><b>c</b></i></sup></a></span> <span class="reference-text"><cite class="citation book cs1"><a rel="nofollow" class="external text" href="http://www.iso.ch/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=21573">"ISO/IEC 13568:2002"</a>. <a rel="nofollow" class="external text" href="http://standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip"><i>Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics</i></a> <span class="cs1-format">(<a href="Zip_(file_format)" class="mw-redirect" title="Zip (file format)">Zipped</a> <a href="PDF" title="PDF">PDF</a>)</span>. ISO. 1 July 2002.</cite> 196 pp.</span>

</li>

<li id="cite_note-Corrigendum-11"><span class="mw-cite-backlink">^ <a href="#cite_ref-Corrigendum_11-0"><sup><i><b>a</b></i></sup></a> <a href="#cite_ref-Corrigendum_11-1"><sup><i><b>b</b></i></sup></a></span> <span class="reference-text"><cite class="citation book cs1">"ISO/IEC 13568:2002/Cor.1:2007". <a rel="nofollow" class="external text" href="http://www.iso.org/iso/iso_catalogue/catalogue_tc/catalogue_detail.htm?csnumber=46112"><i>Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics — Technical corrigendum 1</i></a> <span class="cs1-format">(PDF)</span>. ISO. 15 July 2007.</cite> 12 pp.</span>

</li>

<li id="cite_note-12"><span class="mw-cite-backlink"><b><a href="#cite_ref-12">^</a></b></span> <span class="reference-text"><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://web.archive.org/web/20081202044350/http://web2.comlab.ox.ac.uk/oucl/about/qata92.html">"The Queen's Award for Technological Achievement 1992"</a>. <i><a href="Oxford_University_Computing_Laboratory" class="mw-redirect" title="Oxford University Computing Laboratory">Oxford University Computing Laboratory</a></i>. Archived from <a rel="nofollow" class="external text" href="http://web2.comlab.ox.ac.uk/oucl/about/qata92.html">the original</a> on 2 December 2008<span class="reference-accessdate">. Retrieved <span class="nowrap">17 October</span> 2021</span>.</cite></span>

</li>

</ol></div></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="International_Organization_for_Standardization_(ISO)_standards364" style="padding:3px"><table class="nowraplinks hlist mw-collapsible mw-collapsed navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="International_Organization_for_Standardization_(ISO)_standards364" style="font-size:114%;margin:0 4em"><a href="International_Organization_for_Standardization" title="International Organization for Standardization">International Organization for Standardization</a> (ISO) standards</div></th></tr><tr><td class="navbox-abovebelow" colspan="2"><div>List of <a href="List_of_ISO_standards" title="List of ISO standards">ISO standards</a> – <a href="List_of_ISO_romanizations" title="List of ISO romanizations">ISO romanizations</a> – <a href="List_of_IEC_standards" title="List of IEC standards">IEC standards</a></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">1–9999</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">10000–19999</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">20000–29999</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="ISO/IEC_27000_family" title="ISO/IEC 27000 family">27000 series</a></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">30000+</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div>

<ul><li><span class="noviewer" typeof="mw:File"><span title="Category"></span></span> Category</li></ul>

</div></td></tr></tbody></table></div>

<div class="navbox-styles"></div><div role="navigation" class="navbox" aria-labelledby="IEC_standards56" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="IEC_standards56" style="font-size:114%;margin:0 4em"><a href="List_of_IEC_standards" title="List of IEC standards">IEC standards</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">IEC</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">ISO/IEC</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">

<li><a href="ISO/IEC_27000_family" title="ISO/IEC 27000 family">27000 family</a></li>

</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">

<ul><li><a href="International_Electrotechnical_Commission" title="International Electrotechnical Commission">International Electrotechnical Commission</a></li></ul>

</div></td></tr></tbody></table></div>

<div class="navbox-styles"></div><div role="navigation" class="navbox authority-control" aria-labelledby="Authority_control_databases_frameless&#124;text-top&#124;10px&#124;alt=Edit_this_at_Wikidata&#124;link=https&#58;//www.wikidata.org/wiki/Q1430781#identifiers&#124;class=noprint&#124;Edit_this_at_Wikidata720" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><div id="Authority_control_databases_frameless&#124;text-top&#124;10px&#124;alt=Edit_this_at_Wikidata&#124;link=https&#58;//www.wikidata.org/wiki/Q1430781#identifiers&#124;class=noprint&#124;Edit_this_at_Wikidata720" style="font-size:114%;margin:0 4em">Authority control databases </div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">National</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://d-nb.info/gnd/4225739-6">Germany</a></span></li><li><span class="uid"><a rel="nofollow" class="external text" href="https://id.loc.gov/authorities/sh87007136">United States</a></span></li><li><span class="uid"><a rel="nofollow" class="external text" href="https://www.nli.org.il/en/authorities/987007536597605171">Israel</a></span></li></ul></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"><ul><li><span class="uid"><a rel="nofollow" class="external text" href="https://lux.collections.yale.edu/view/concept/562c1980-19a4-4958-98a6-0337df9690e8">Yale LUX</a></span></li></ul></div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-07-17" href="https://en.wikipedia.org/wiki/?title=Z_notation&oldid=1300907235">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>